Nuprl Lemma : es-alive-val
11,40
postcript
pdf
es
:ES,
Fail
:AbsInterface(Top),
A
:Type,
X
:AbsInterface(
A
),
e
:E.
(
(
e
alive(
X
)))
(alive(
X
)(
e
) =
X
(
e
)
A
)
latex
Definitions
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
E
,
ES
,
AbsInterface(
A
)
,
Type
,
fail-dcdr{i:l}(
es
;
Fail
)
,
Dec(
P
)
,
x
:
A
B
(
x
)
,
b
,
e
X
,
(
e
<loc
e'
)
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
Top
,
,
x
.
A
(
x
)
,
x
.
t
(
x
)
,
(
I
|
p
)
,
a
:
A
fp
B
(
a
)
,
X
(
e
)
,
<
a
,
b
>
,
strong-subtype(
A
;
B
)
,
P
Q
,
alive(
X
)
,
A
,
{
x
:
A
|
B
(
x
)}
,
E(
X
)
,
left
+
right
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
t
.1
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
if
b
then
t
else
f
fi
,
Void
,
False
,
A
c
B
,
P
Q
,
P
Q
Lemmas
iff
wf
,
rev
implies
wf
,
es-interface-val-co-restrict
,
es-interface-val
wf2
,
es-is-interface-co-restrict
,
member
wf
,
es-E-interface
wf
,
subtype
rel
wf
,
event
system
wf
,
es-interface
wf
,
es-interface-val
wf
,
es-interface-co-restrict
wf
,
es-locl
wf
,
assert
wf
,
top
wf
,
es-is-interface
wf
,
fail-dcdr
wf
,
es-E
wf
origin
es:ES, Fail:AbsInterface(Top), A:Type, X:AbsInterface(A), e:E.
(e 
alive(X))) 
(alive(X)(e) = X(e) A) es:ES, Fail:AbsInterface(Top), A:Type, X:AbsInterface(A), e:E.
(e alive(X))) (alive(X)(e) = X(e) A) 
B(x)
B(x)
x:A. B(x)
x.A(x)
x. t(x)
p)
B